\begin{tabbing}
$\forall$\=$R$:es\_realizer\{i:l\}, ${\it sv}$:(Id$\rightarrow$($T$:Type\{i\} $\times$ ($T$ + ($\mathbb{Q}\rightarrow$$T$)))), ${\it av}$:(Knd$\rightarrow$Type\{i\}),\+
\\[0ex]${\it dis}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$), ${\it cl}$:(Id$\rightarrow$($n$:$\mathbb{Z}$ $\times$ base{-}domain{-}type($n$))$\rightarrow$es\_realizer\{i:l\}), ${\it fr}$,
\\[0ex]${\it rfr}$:(Id$\rightarrow$Id$\rightarrow$(Knd List)), ${\it sfr}$:(IdLnk$\rightarrow$Id$\rightarrow$(Knd List)), ${\it afr}$:(Id$\rightarrow$Knd$\rightarrow$((Id List) + Top)),
\\[0ex]${\it bfr}$:(Id$\rightarrow$Knd$\rightarrow$((IdLnk List) + Top)).
\-\\[0ex]R{-}FeasibleWitness\{i:l\}($R$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$) $\in$ $\mathbb{P}$\{i'\}
\end{tabbing}